Nuprl Lemma : isrcv_wf
0,22
postcript
pdf
k
:Knd. isrcv(
k
)
latex
Definitions
Knd
,
isrcv(
k
)
,
isl(
x
)
,
x
:
A
.
B
(
x
)
,
IdLnk
,
t
T
,
Id
Lemmas
Id
wf
,
IdLnk
wf
,
isl
wf
origin
k:Knd. isrcv(k) 
k:Knd. isrcv(k) x:A. B(x) T